package interfaces.managers;

import interfaces.ICliente;
import interfaces.IIncidencia;
import interfaces.ITecnico;

import java.util.List;

import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;

public interface IBuscadorIncidenciasWithModel extends IBuscadorIncidencias, IBuscadorIncidenciasModel {
	@Pre ({"codigoIncidencia >= 0 && codigoIncidencia <= Integer.MAX_VALUE"})
	@Pos ({"encontrado(codigoIncidencia) != null ==> result == encontrado(codigoIncidencia) && !result.isEmpty()", "encontrado(codigoIncidencia) == null ==> result == null"})
	public List<IIncidencia> buscaIncidencia(int codigoIncidencia);
	@Pre ({"i != null #NullPointerException", "estaRegistrado(i)"})
	@Pos ({"encontrado(i) != null ==> result == encontrado(i) && !result.isEmpty()", "encontrado(i) == null ==> result == null"})
	public List<IIncidencia> buscaIncidencia(IIncidencia i);
	@Pre ({"p != null #NullPointerException", "estaRegistrado(p)"})
	@Pos ({"encontrado(p) != null ==> result == encontrado(p) && !result.isEmpty()", "encontrado(i) == null ==> result == null"})
	public List<IIncidencia> buscaIncidencia(ITecnico p);
    @Pre ({"p != null #NullPointerException", "estaRegistrado(c)"})
	@Pos ({"encontrado(p) != null ==> result == encontrado(p) && !result.isEmpty()", "encontrado(i) == null ==> result == null"})
	public List<IIncidencia> buscaIncidencia(ICliente c);
}
